explanation of antecedent functions
11,40
Antecedent functions are .....
so we define it like this: antecedent-function(
es
;
A
;
B
;
e
.
P
(
e
);
e
.
Q
(
e
);
e
.
f
(
e
);
R
) {FDLNOr16675}
It's wf lemma is : antecedent-function_wf
origin